輪講 - 論理と計算のしくみ 5.3 型付きλ計算 (前半) (外部記事)
https://www.slideshare.net/oarat/53-56830331
#外部記事
論理と計算のしくみ(本)
伊奈 林太郎
単純型付きλ計算
の
強正規可能性
を示している
おれは面倒だったので
単純型付きλ計算における値呼び簡約の停止性
（
値呼び簡約
の停止性だけを示している）
教科書はこっちでやっており，
強正規可能性
は演習問題としている